Search for: All records

Online learning has become desirable for many students. In the U.S., more than one-third of all enrolled students participate in at least one online course [13]. The most effective online learning environments allow students to work at their own pace, from any location, at any time, and to receive automated feedback. In light of these benefits and the likely protracted impact of the current public health crisis, the trend toward online learning is likely to increase. 

To develop code that meets its specification and is verifiably correct, such as in a software engineering course, students must be able to understand formal contracts and annotate their code with assertions such as loop invariants. To assist in developing suitable instructor and automated tool interventions, this research aims to go beyond simple pre- and post-conditions and gain insight into student learning of loop invariants involving objects. As students develop suitable loop invariants for given code with the aid of an online system backed by a verification engine, each student attempt, either correct or incorrect, was collected and analyzed automatically, and catalogued using an iterative process to capture common difficulties. Students were also asked to explain their thought process in arriving at their answer for each submission. The collected explanations were analyzed manually and found to be useful to assess their level of understanding as well as to extract actionable information for instructors and automated tutoring systems. Qualitative conclusions include the impact of the medium. 

One aspect of developing correct code, code that functions as specified, is annotating loops with suitable invariants. Loop invariants are useful for human reasoning and are necessary for tool-assisted automated reasoning. Writing loop invariants can be a difficult task for all students, especially beginning software engineering students. In helping students learn to write adequate invariants, we need to understand not only what errors they make, but also why they make them. This poster discusses the use of a Web IDE backed by the RESOLVE verification engine to aid students in developing loop invariants and to collect performance data. In addition to collecting submitted invariant answers, students are asked to provide their steps or thought processes regarding how they arrived at their answers for each submission. The answers and reasons are then analyzed using a mixed-methods approach. Resulting categories of answers indicate that students are able to use formal method concepts with which they are already familiar, such as, pre and post-conditions as a starting place to develop adequate loop invariants. Additionally, some common trouble spots in learning to write invariants are identified. The results will be useful to guide classroom instruction and automated tutoring. 

Object-based development using design-by-contract (DbC) is broadly taught and practiced. Students must be able to read and write symbolic DbC assertions that are sufficiently precise and be able to use these assertions to trace program code. This paper summarizes the results of using an automated tool to pinpoint fine-grain difficulties students face in learning to symbolically trace code involving objects. The pilots were conducted in an undergraduate software engineering course. Quantitative results show that data collected by the tool can help to identify and classify learning obstacles. Qualitative findings help validate student misunderstandings underlying these difficulties. Analysis of exam questions helps understand the persistence of student learning to read and write simple assertions about code behavior. Together, these results provide directions for intervention.